HW#5 --- last modified March 02 2019 21:25:49..

Solution set.

Due date: May 15

Files to be submitted:
  Hw5.tex
  Sat.zip

Purpose: To practice applying the theory of NP-completeness. To investigate threshold phenomenon for satisfiability. To implement reductions and to experiment with approximation algorithms.

Specification: First do the following problems out of CLRS and submit them in Hw5.tex: 34.2-8, 34.4-6, 34.5-1, 35.1-1.

The coding part of this assignment should be zipped together and submitted in the file Sat.zip . For the coding assignment I would like you to implement three classes: ThreeSat, VertexCover, and Tester. The first constructor for ThreeSat takes a n by 3 array of int's and stores it to a local field, int instance[][]. You should have a method getInstance which returns this array. The intended meaning of the array is a sequence of n clauses. Each clause has at most three variables or their negations in it. For instance, instance[6][0] == 7, instance[6][1] == -3, instance[6][0] == 0 would mean the 6+1th clause of this instance of 3SAT has variable 7, the negation of variable 3, and no third variable. (0 means no variable in the given slot). A literal is either a variable or its negation. Your constructor should look through the array during the construction process and determine the largest literal number and store this in the field variable maxLiteralUsed. You should have a public method getMaxLiteralUsed which returns this positive integer. The second constructor for your class ThreeSat should take two int's numVariables, and numClauses. Given these two inputs it should set maxLiteralUsed to numVariables. It should then do instance = new int[numClauses][3]; and randomly fill each value of this array with a value in the range -numVariables to numVariables.

Besides the constructors, ThreeSat should have public methods:

boolean evaluate(boolean assignment[])

and

boolean isSatisfiable() .

evaluate() takes an array, assignment[], which should be of size maxLiteralUsed. assignment[] is supposed to give the truth settings for each of the variables in instance[][], where assignment[i] is the value of variable i+1 . Given this information evaluate is supposed to say if the ThreeSat instance evaluates to true or false.

isSatisfiable() is supposed to return true if there is some truth assignment which can make the ThreeSat instance true; and returns false otherwise. To implement isSatisfiable you can just do a brute force check over all possible assignments. This method should call evaluate().

The class VertexCover should have a constructor which takes an n x n array instance[][] of booleans. The constructor should store this array in a local field also called instance[][]. It should then check that the array is a square matrix and that it is symmetric; that is, intance[i][j] = instance[j][i]. If these fail a BadGraphException should be thrown. instance[][] is supposed to represent an undirected graph. The number of vertices in the graph is the size of a dimension of this matrix. The value of instance[i][j] is true if there is an edge between i and j; and false otherwise.

Besides the constructor, VertexCover should have two public methods:

boolean hasCover(int k);

int[] approxCover();

hasCover(k) should return true if the stored graph has a vertex cover of size k. To check for this I want you to compute a reduction from VertexCover to ThreeSat (this is the opposite direction to the reductions 3SAT to CLIQUE to VERTEX_COVER). Then use the ThreeSat isSatisfiable algorithm to check if the vertex cover exists.

approxCover() should implement the approximate vertex cover algorithm from the book and return a vertex cover as an array of vertex numbers for the vertices in the cover.

Finally, your Tester program should be runnable from the command line with a line like:

java Tester

It should launch a little JFrame application with a menu bar. From the menu bar you should be to select "Graph Sat Instances". Selecting this should cause your program to draw a graph of where along the x axis is the clause to variable ratio and has values between 1 and 10. The y-axis should have values between 0 and 1 indicating over 100 trials the number of random 3SAT instances with that clause to variable ratio that were satisfiable. You should you fix your number of clauses for all points you plot to some value which makes the above not take more than 3-5 minutes to run. (On the other hand, it shouldn't be too small so that the results don't look interesting.) The menu bar should also have a item "Test for Vertex Cover". This should pop up a window that let's you pick a text file with graph data in it. Using this file's data your program should call hasCover and approxCover and display the results. The format of the text file should be one line per matrix row. Each row should have 0's and 1's and be comma separated. A 1 indicates an edge a 0 no edge. For example below is a small graph as a text file:

0,1,0
1,0,1
0,1,0

Point Breakdown